package com.googlecode.kipler.satisfiability.interpolation.rule;

import java.util.Iterator;

import com.googlecode.kipler.container.dl.BasicWcsInterpolationData;
import com.googlecode.kipler.container.dl.LabelManager;
import com.googlecode.kipler.syntax.concept.RoleQuantification;
import com.googlecode.kipler.syntax.concept.RoleQuantification.Constructor;
import com.googlecode.kipler.syntax.formula.ConceptAssertion;
import com.googlecode.kipler.syntax.formula.Formula;
import com.googlecode.kipler.syntax.formula.ObjectRoleAssertion;

public class SomeValuesInterpolantRule extends InterpolantRule {

	@Override
	public ConceptAssertion apply() {
		BasicWcsInterpolationData wcsData = (BasicWcsInterpolationData) getWcs()
				.getData();
		LabelManager labelMan = wcsData.getLabelManager();
		Iterator<Formula> fIter = getCondition().iterator();
		ConceptAssertion firstFormula = (ConceptAssertion) fIter.next();
		ObjectRoleAssertion secondFormula = (ObjectRoleAssertion) fIter.next();
		ConceptAssertion result = getPreviousInterpolants().iterator().next();
		if (secondFormula.getFiller().equals(result.getName())) {
			if (labelMan.isLeftDerived(firstFormula)) {
				result.setConcept(new RoleQuantification(Constructor.SOME,
						secondFormula.getRole(), result.getConcept()));
			} else {
				result.setConcept(new RoleQuantification(Constructor.ALL,
						secondFormula.getRole(), result.getConcept()));
			}
		}
		return result;
	}

}
